\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $T$:Type, ${\it ks}$:(Knd List), ${\it upd}$:update{-}spec(\=${\it ds}$;\+\+
\\[0ex]${\it da}$
\\[0ex]),
\-\\[0ex]$a$:($\mathbb{N}\rightarrow$($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$)\} $\rightarrow$decl{-}state(${\it ds}$)$\rightarrow$ma{-}valtype(${\it da}$; $k$)$\rightarrow$$T$$\rightarrow\mathbb{B}$)).
\-\\[0ex]($\neg$($\uparrow$fpf{-}dom(id{-}deq; mkid\{ecl:ut2\}; ${\it ds}$)))
\\[0ex]$\Rightarrow$ normal{-}type\=\{i:l\}\+
\\[0ex]($T$)
\-\\[0ex]$\Rightarrow$ normal{-}ds\=\{i:l\}\+
\\[0ex](${\it ds}$)
\-\\[0ex]$\Rightarrow$ normal{-}da\=\{i:l\}\+
\\[0ex](${\it da}$)
\-\\[0ex]$\Rightarrow$ l\_all(${\it ks}$; Knd; $k$.(($\uparrow$isrcv($k$)) $\Rightarrow$ ($i$ = destination(lnk($k$)) $\in$ Id)))
\\[0ex]$\Rightarrow$ update{-}spec{-}decl(${\it upd}$; ${\it ds}$)
\\[0ex]$\Rightarrow$ R{-}realizes\=\{i:l\}\+
\\[0ex](\=ecl{-}machine2($i$; ${\it ds}$; ${\it da}$; mkid\{ecl:ut2\}; $T$; ${\it ks}$; $a$; ${\it upd}$);\+
\\[0ex]${\it es}$.l\_all
\\[0ex](\=update{-}spec{-}vars(${\it upd}$);\+
\\[0ex]Id;
\\[0ex]$z$.(es{-}decls(${\it es}$;$i$;fpf{-}join(id{-}deq; ${\it ds}$; fpf{-}single(mkid\{ecl:ut2\}; $T$));${\it da}$)
\\[0ex]$\Rightarrow$ \=(subtype\_rel(es{-}vartype(${\it es}$; $i$; $z$); fpf{-}ap(${\it ds}$; id{-}deq; $z$))\+
\\[0ex]c$\wedge$ \=(($\uparrow$bor(($\neg_{b}$null(${\it ks}$)); es{-}isconst(${\it es}$; $i$; $z$)))\+
\\[0ex]$\Rightarrow$ alle{-}at(\=${\it es}$;\+
\\[0ex]$i$;
\\[0ex]$e$.$\forall$${\it e'}$$\geq$$e$.\=es{-}after(${\it es}$; $z$; ${\it e'}$)\+
\\[0ex]=
\\[0ex]es{-}trans{-}state{-}from\{i:l\}(\=${\it es}$;${\it ks}$;\+
\\[0ex]$\lambda$$k$,$s$,$v$,${\it z'}$. list\_accum
\\[0ex](\=${\it z'}$,${\it nf}$.let $n$,$f$ = ${\it nf}$\+
\\[0ex]in
\\[0ex]if \=$a$\+
\\[0ex]($n$
\\[0ex],$k$
\\[0ex],$s$
\\[0ex],$v$
\\[0ex],$s$(mkid\{ecl:ut2\}))
\-\\[0ex]then $f$($s$,$v$)
\\[0ex]else ${\it z'}$
\\[0ex]fi ;
\\[0ex]${\it z'}$;
\\[0ex]fpf{-}cap(\=${\it upd}$;\+
\\[0ex]product{-}deq
\\[0ex](\=Knd;\+
\\[0ex]Id;
\\[0ex]Kind{-}deq;
\\[0ex]id{-}deq);
\-\\[0ex]$<$$k$, $z$$>$;
\\[0ex][]));es{-}when(\=${\it es}$;\+
\\[0ex]$z$;
\\[0ex]$e$
\\[0ex]);$e$;${\it e'}$)
\-\-\-\-\\[0ex]$\in$ fpf{-}ap(${\it ds}$; id{-}deq; $z$)))))))
\-\-\-\-\-\-\-
\end{tabbing}